nLab Jasper Hugunin

• personal page

Selected writings

On higher inductive-inductive types in cubical type theory:

• Jasper Hugunin, Constructing Inductive-Inductive Types in Cubical Type Theory, in Foundations of Software Science and Computation Structures. FoSSaCS 2019, Lecture Notes in Computer Science 11425 (2019) [doi:10.1007/978-3-030-17127-8_17]

On W-types:

• Jasper Hugunin, Why Not W?, Leibniz International Proceedings in Informatics (LIPIcs) 188 (2021) [doi:10.4230/LIPIcs.TYPES.2020.8, pdf]

• Jasper Hugunin, IWTypes, https://github.com/jashug/IWTypes

category: people